es:ES, a:Atom1, e:E.
e sends a
 loc(e) >> a
  (e':E. (e' < e) & e' sends a to loc(e))
  (state when es-init(es;e)):state@loc(es-init(es;e))>>a 

latex

Definitions	x:A. B(x), P  Q, P  Q, x:A. B(x), P & Q, t  T, Prop, {T}, e sends a to i, A & B, e receives a, e  e' , Trans x,y:T. E(x;y), (e <loc e')
Lemmas	es-atom-lemma1, inheres wf, es-state wf, es-loc wf, es-state-when wf, atom-free-es-state, es-E wf, es-causl wf, es-send-atom-to wf, es-init wf, es-atom wf, es-send-atom wf, event system wf, es-sender wf, es-axioms, es-sender-causl, es-le-loc, Id wf